A:Type, eq:EqDecider(A), B:(AType), L:(a:A fp B(a) List), x:A.
(x  fpf-domain((L)))  (fL.(x  dom(f)) & (L)(x) = f(x)  B(x)) 

latex

Definitions	x:A. B(x), x(s), t  T, x. t(x), P  Q, S  T, P  Q, P  Q, P & Q,
Lemmas	fpf-join-list-ap, fpf wf, deq wf, l member wf, fpf-domain wf, fpf-join-list wf, top wf, fpf-trivial-subtype-top, member-fpf-domain